from cheqed.core.plan import Assumption, Compound, Rule, Branch
from cheqed.core.tactic import applicable
from cheqed.core import side, tactic
from cheqed.core.rules.match import match_first

parse = tactic.parse
prettyprint = tactic.prettyprint

def assumption():
    return Assumption()
    
def compound(func, repr_):
    return Compound(func, repr_)

def rule(func, repr_):
    return Rule(func, repr_)

def branch(first, *branches):
    return Branch(first, *branches)

def pair(first, second):
    return branch(first, second)

def sequence(*seq):
    if len(seq) == 0:
        raise 'sequence error: nothing to do.'
    if len(seq) == 1:
        return seq[0]
    return pair(seq[0], sequence(*seq[1:]))

# ---

from cheqed.core.rules import primitive

rules = []

import inspect

def register(func):
    print 'registering %s' % func.func_name

    arg_names, varargs, varkw, defaults = inspect.getargspec(func)

    if not hasattr(func, 'arg_names'):
        func.arg_names = arg_names
    
    rules.append(func)
    return func

# Structural Rules

@register
def left_contraction():
    return rule(primitive.left_contraction, 'left_contraction()')

@register
def right_contraction():
    return rule(primitive.right_contraction, 'right_contraction()')

@register
def left_weakening():
    return rule(primitive.left_weakening, 'left_weakening()')

@register
def right_weakening():
    return rule(primitive.right_weakening, 'right_weakening()')

@register
def left_permutation(index):
    return rule(lambda x: primitive.left_permutation(x, index),
                'left_permutation(%d)' % index)

@register
def right_permutation(index):
    return rule(lambda x: primitive.right_permutation(x, index),
                'right_permutation(%d)' % index)

# Logical Rules

@register
def axiom():
    return rule(primitive.axiom, 'axiom()')

@register
def left_negation():
    return rule(primitive.left_negation, 'left_negation()')

@register
def right_negation():
    return rule(primitive.right_negation, 'right_negation()')

@register
def left_disjunction():
    return rule(primitive.left_disjunction, 'left_disjunction()')

@register
def right_disjunction():
    return rule(primitive.right_disjunction, 'right_disjunction()')

@register
@applicable(side.LEFT, 'for_all x . phi')
def left_universal(witness):
    return rule(lambda x: primitive.left_universal(x, witness),
                "left_universal(parse(r'%s'))" % prettyprint(witness))

@register
@applicable(side.RIGHT, 'for_all x . phi')
def right_universal(witness):
    return rule(lambda x: primitive.right_universal(x, witness),
                "right_universal(parse(r'%s'))" % prettyprint(witness))

@register
@applicable(side.LEFT, 'schema phi . psi')
def left_schema(witness):
    return rule(lambda x: primitive.left_schema(x, witness),
                "left_schema(parse(r'%s'))" % prettyprint(witness))

@register
def left_separation():
    return rule(primitive.left_separation, 'left_separation()')

@register
def right_separation():
    return rule(primitive.right_separation, 'right_separation()')

@register
def left_substitution():
    return rule(primitive.left_substitution, 'left_substitution()')

@register
def right_substitution():
    return rule(primitive.right_substitution, 'right_substitution()')

@register
def cut(name):
    return rule(lambda x: tactic._cut(x, tactic.definitions[name]),
                "cut('%s')" % name)

# Derived Rules

def make_compound(func):
    arg_names, varargs, varkw, defaults = inspect.getargspec(func)
    arg_names.remove('goal')
    assert varargs is None
    assert varkw is None
    assert defaults is None

    def new_func(*args):
        pretty_args = []
        for arg, name in zip(args, arg_names):
            if name == 'witness':
                pretty_args.append("parse(r'%s')" % prettyprint(arg))
            elif name == 'index':
                pretty_args.append(str(arg))

        pretty = '%s(%s)' % (func.func_name,
                             ', '.join(pretty_args))
                
        return compound(lambda goal: func(goal, *args), pretty)
    new_func.func_name = func.func_name
    new_func.arg_names = arg_names
    return new_func

@register
@make_compound
def left_conjunction(goal):
    return sequence(cut('logic.and.definition'),
                    left_permutation(1),
                    left_substitution(),
                    left_permutation(1),
                    left_weakening(),
                    left_negation(),
                    right_disjunction(),
                    right_negation(),
                    right_negation(),
                    left_permutation(1))

@register
@make_compound
def right_conjunction(goal):
    return sequence(cut('logic.and.definition'),
                    right_substitution(),
                    left_weakening(),
                    right_negation(),
                    branch(left_disjunction(),
                          left_negation(),
                          left_negation()))

@register
@make_compound
def left_implication(goal):
    return sequence(cut('logic.implies.definition'),
                    left_permutation(1),
                    left_substitution(),
                    left_permutation(1),
                    left_weakening(),
                    branch(left_disjunction(),
                           left_negation(),
                           assumption()))

@register
@make_compound
def right_implication(goal):
    return sequence(cut('logic.implies.definition'),
                    right_substitution(),
                    left_weakening(),
                    right_disjunction(),
                    right_negation())

@register
@make_compound
def right_bidirectional(goal):
    return sequence(cut('logic.iff.definition'),
                    right_substitution(),
                    left_weakening(),
                    branch(right_conjunction(),
                          right_implication(),
                          right_implication()))

@register
@make_compound
def left_bidirectional(goal):
    return sequence(cut('logic.iff.definition'),
                    left_permutation(1),
                    left_substitution(),
                    left_permutation(1),
                    left_weakening(),
                    left_conjunction(),
                    branch(left_implication(),
                           branch(left_implication(),
                                  right_permutation(1),
                                  axiom()),
                           sequence(left_permutation(1),
                                    branch(left_implication(),
                                           axiom(),
                                           assumption()))))


@applicable(side.RIGHT, 'exists x . phi')
@register
@make_compound
def right_existential(goal, witness):
    return sequence(right_contraction(),
                    cut('logic.exists.definition'),
                    right_substitution(),
                    left_weakening(),
                    right_negation(),
                    left_universal(witness),
                    left_negation(),
                    left_weakening())

@applicable(side.LEFT, 'exists x . phi')
@register
@make_compound
def left_existential(goal, witness):
    return sequence(cut('logic.exists.definition'),
                    left_permutation(1),
                    left_substitution(),
                    left_permutation(1),
                    left_weakening(),
                    left_negation(),
                    right_universal(witness),
                    right_negation())

@register
@make_compound
def left_subset(goal):
    return sequence(cut('set.subset.definition'),
                    left_permutation(1),
                    left_substitution(),
                    left_permutation(1),
                    left_weakening(),
                    left_universal(parse(r'foo')),
                    left_permutation(1),
                    left_weakening(),
                    left_implication())

@register
@make_compound
def right_subset(goal):
    return sequence(cut('set.subset.definition'),
                    right_substitution(),
                    left_weakening(),
                    right_universal(parse(r'foo')),
                    right_implication())

@register
@make_compound
def qed(goal):
    for i, left in enumerate(goal.left):
        for j, right in enumerate(goal.right):
            if left == right:
                return sequence(left_permutation(i),
                                right_permutation(j),
                                axiom())
    raise Exception('qed does not apply.')

propositional_rules = [
    (left_negation, 1),
    (right_negation, 1),
    (left_disjunction, 2),
    (right_disjunction, 1),
    (left_conjunction, 1),
    (right_conjunction, 2),
    (left_implication, 2),
    (right_implication, 1),
    (left_bidirectional, 2),
    (right_bidirectional, 2),
    ]

@register
@make_compound
def solve_propositional(goal):
    plan = assumption()
    applicable = []
    for rule, cost in propositional_rules:
        if is_applicable(rule, plan, goal):
            applicable.append((cost, rule))
    applicable.sort()

    if len(applicable) > 0:
        return applicable[0][1]()

    raise Exception('no applicable propositional rule')

@register
@make_compound
def right_extension(goal):
    match = match_first(goal, side.RIGHT, 'a = b')
    return sequence(cut('zfc.extensionality'),
                    left_universal(match['a']),
                    left_permutation(1),
                    left_weakening(),
                    left_universal(match['b']),
                    left_permutation(1),
                    left_weakening(),
                    left_universal(parse(r'foo')),
                    left_permutation(1),
                    left_weakening(),
                    branch(left_implication(),
                           right_bidirectional(),
                           axiom()))

@register
@make_compound
def left_powerset(goal):
    match = match_first(goal, side.LEFT, 'a in powerset(b)')
    return sequence(cut('set.powerset.definition'),
                    left_universal(match['b']),
                    left_permutation(1),
                    left_weakening(),
                    left_universal(match['a']),
                    left_permutation(1),
                    left_weakening(),
                    branch(left_bidirectional(),
                           axiom(),
                           left_weakening()))

@register
@make_compound
def right_powerset(goal):
    match = match_first(goal, side.RIGHT, 'a in powerset(b)')
    return sequence(cut('set.powerset.definition'),
                    left_universal(match['b']),
                    left_permutation(1),
                    left_weakening(),
                    left_universal(match['a']),
                    left_permutation(1),
                    left_weakening(),
                    branch(left_bidirectional(),
                           right_weakening(),
                           axiom()))
                                   




def evaluate(string):
    try:
        return eval(string)
    except:
        raise Exception('evaluate failed: ' + string)

def is_applicable(func, prover, goal):
    if hasattr(func, 'is_applicable'):
        return func.is_applicable(prover.subgoals(goal)[0])

    if len(func.arg_names) > 0:
        return True

    try:
        tester = prover.replace(prover.assumptions()[0], func())
        tester.subgoals(goal)
    except Exception, e:
        return False

    return True

def applicable_rules(prover, goal):
    subgoals = prover.subgoals(goal)
    if len(subgoals) == 0:
        return []
    
    applicable = []
    for func in rules:
        if is_applicable(func, prover, goal):
            applicable.append((func.func_name, func.arg_names))

    return applicable
